Peirce's law

Axiom

Pierce's law is expressed as the following: proposition $p$ must be true if there is a proposition $q$ such that if truth of $p$ follows from the truth of "if $p$ then $q$", i.e.

(holds in classical propositional logic)

Notes

• Peirce's law holds in classical propositional calculus, but not in intuitionistic propositional calculus
• It is logically equivalent to the law of excluded middle, $\vdash p \lor \neg p$

See also

• Curry-Howard correspondence

References

1. https://en.wikipedia.org/wiki/Peirce's_law
2. https://inquiryintoinquiry.com/2008/10/06/peirces-law/
3. https://proofwiki.org/wiki/Peirce's_Law